/*
 * Copyright (c) 2009, Palle Raabjerg
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 *   * Redistributions of source code must retain the above copyright notice,
 *     this list of conditions and the following disclaimer.
 *   * Redistributions in binary form must reproduce the above copyright notice,
 *     this list of conditions and the following disclaimer in the documentation
 *     and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
 * POSSIBILITY OF SUCH DAMAGE.
 */

/* spiparser.mly */
/* Spi Calculus parser */
%{
open Printf
let parse_error s = (* Called by the parser function on error *)
  print_endline ("spiparser: " ^ s);
  flush stdout;;
%}
%token <string> ID
%token <string> LVAR
%token <char> CHAR
%token NIL OK
%token BEGIN END BANG PAR OUT IN NEW DECRYPT SPLIT MATCH
%token CHAN UN KEY TOK TPAIR UNKNOWN
%token EMPTY PAIR COMMA LPAREN RPAREN LBRACE RBRACE COLON SCOLON AS DASH EXPECT

%start process
%start msgtype
%start resource
%start message
%type <Spitree.proc> process
%type <Spitree.typ> msgtype
%type <Spitree.datalog> resource
%type <Spitree.msg> message

%start dprogram
%type <Spitree.term> term
%type <Spitree.literal> literal
%type <Spitree.term list> restlit
%type <Spitree.hclause> hclause
%type <Spitree.literal list> restcl
%type <Spitree.datalog> dprogram
%type <Spitree.hclause list> restprog

%%
process:    NIL  { Spitree.PNil }
	  | OUT LPAREN message COMMA message RPAREN  { Spitree.Out($3, $5) }
	  | IN LPAREN message COMMA ID RPAREN SCOLON process  { Spitree.In($3, $5, $8) }
	  | BANG IN LPAREN message COMMA ID RPAREN SCOLON process  { Spitree.InRepl($4, $6, $9) }
	  | NEW ID COLON msgtype SCOLON process  { Spitree.Nu($2, $4, $6) }
	  | LPAREN process parrest { if $3 = Spitree.PNil then
				       $2
				     else
				       Spitree.PPara($2, $3) }
	  | BEGIN ID LPAREN message RPAREN  { Spitree.Datprog([[($2, [Spitree.SpiMsg($4)])]]) }
	  | END ID LPAREN message RPAREN  { Spitree.Expect($2, [Spitree.SpiMsg($4)]) }
	  | DECRYPT message AS LBRACE ID COLON msgtype RBRACE message SCOLON process  { Spitree.Decrypt($2, $5, $7, $9, $11) }
	  | SPLIT message AS LPAREN ID COLON msgtype COMMA ID COLON msgtype RPAREN SCOLON process  { Spitree.Split($2, $5, $7, $9, $11, $14) }
	  | MATCH message COLON msgtype AS LPAREN message COMMA ID COLON msgtype RPAREN SCOLON process  { Spitree.Match($2, $4, $7, $9, $11, $14) }
	  | EXPECT ID LPAREN restlit { if (List.for_all (fun term ->
							   match term with
							     | Spitree.SpiMsg(_) -> true
							     | _ -> false
							) $4)
				       then (Spitree.Expect($2, $4))
				       else raise Parsing.Parse_error }
	  | dprogram { Spitree.Datprog($1) }
;
parrest:    PAR process parrest { if $3 = Spitree.PNil then
				    $2
				  else
				    Spitree.PPara($2, $3) }
	  | RPAREN { Spitree.PNil }
;
msgtype:    UN  { Spitree.Un }
	  | UNKNOWN  { Spitree.Unknown }
	  | KEY LPAREN msgtype RPAREN  { Spitree.Key($3) }
	  | TPAIR LPAREN ID COLON msgtype COMMA msgtype RPAREN  { Spitree.TPair($3, $5, $7) }
	  | TOK LPAREN dprogram RPAREN  { Spitree.TOk($3) }
	  | TOK LPAREN resource RPAREN  { Spitree.TOk($3) }
	  | CHAN LPAREN msgtype RPAREN  { Spitree.Ch($3) }
;
resource:   EMPTY  { [] }
	  | LPAREN resource COMMA resource RPAREN  { List.append $2 $4 }
	  | ID LPAREN message RPAREN  { [[($1, [Spitree.SpiMsg($3)])]] }
;
message:    OK  { Spitree.Ok }
	  | LBRACE message RBRACE message  { Spitree.Encr($2, $4) }
	  | PAIR LPAREN message COMMA message RPAREN  { Spitree.MPair($3, $5) }
	  | ID  { Spitree.Name($1) }
;

term:       LVAR { Spitree.Var($1) }
	  | message { Spitree.SpiMsg($1) }
;
literal:    ID LPAREN restlit { ($1, $3) };
restlit:    term RPAREN { [$1] }
	  | term COMMA restlit { $1::$3 };
hclause:    literal COLON DASH restcl { ($1::$4) }
	  | literal { [$1] };
restcl:     literal COMMA restcl { $1::$3 }
	  | literal { [$1] };
dprogram:   LBRACE restprog { $2 }
restprog:   hclause SCOLON restprog { $1::$3 }
	  | hclause RBRACE { [$1] }
	  | RBRACE { [] };
%%
